| 1: | active(f(X)) | → mark(if(X,c,f(true))) | |
| 2: | active(if(true,X,Y)) | → mark(X) | |
| 3: | active(if(false,X,Y)) | → mark(Y) | |
| 4: | active(f(X)) | → f(active(X)) | |
| 5: | active(if(X1,X2,X3)) | → if(active(X1),X2,X3) | |
| 6: | active(if(X1,X2,X3)) | → if(X1,active(X2),X3) | |
| 7: | f(mark(X)) | → mark(f(X)) | |
| 8: | if(mark(X1),X2,X3) | → mark(if(X1,X2,X3)) | |
| 9: | if(X1,mark(X2),X3) | → mark(if(X1,X2,X3)) | |
| 10: | proper(f(X)) | → f(proper(X)) | |
| 11: | proper(if(X1,X2,X3)) | → if(proper(X1),proper(X2),proper(X3)) | |
| 12: | proper(c) | → ok(c) | |
| 13: | proper(true) | → ok(true) | |
| 14: | proper(false) | → ok(false) | |
| 15: | f(ok(X)) | → ok(f(X)) | |
| 16: | if(ok(X1),ok(X2),ok(X3)) | → ok(if(X1,X2,X3)) | |
| 17: | top(mark(X)) | → top(proper(X)) | |
| 18: | top(ok(X)) | → top(active(X)) | |
| 19: | ACTIVE(f(X)) | → IF(X,c,f(true)) | |
| 20: | ACTIVE(f(X)) | → F(true) | |
| 21: | ACTIVE(f(X)) | → F(active(X)) | |
| 22: | ACTIVE(f(X)) | → ACTIVE(X) | |
| 23: | ACTIVE(if(X1,X2,X3)) | → IF(active(X1),X2,X3) | |
| 24: | ACTIVE(if(X1,X2,X3)) | → ACTIVE(X1) | |
| 25: | ACTIVE(if(X1,X2,X3)) | → IF(X1,active(X2),X3) | |
| 26: | ACTIVE(if(X1,X2,X3)) | → ACTIVE(X2) | |
| 27: | F(mark(X)) | → F(X) | |
| 28: | IF(mark(X1),X2,X3) | → IF(X1,X2,X3) | |
| 29: | IF(X1,mark(X2),X3) | → IF(X1,X2,X3) | |
| 30: | PROPER(f(X)) | → F(proper(X)) | |
| 31: | PROPER(f(X)) | → PROPER(X) | |
| 32: | PROPER(if(X1,X2,X3)) | → IF(proper(X1),proper(X2),proper(X3)) | |
| 33: | PROPER(if(X1,X2,X3)) | → PROPER(X1) | |
| 34: | PROPER(if(X1,X2,X3)) | → PROPER(X2) | |
| 35: | PROPER(if(X1,X2,X3)) | → PROPER(X3) | |
| 36: | F(ok(X)) | → F(X) | |
| 37: | IF(ok(X1),ok(X2),ok(X3)) | → IF(X1,X2,X3) | |
| 38: | TOP(mark(X)) | → TOP(proper(X)) | |
| 39: | TOP(mark(X)) | → PROPER(X) | |
| 40: | TOP(ok(X)) | → TOP(active(X)) | |
| 41: | TOP(ok(X)) | → ACTIVE(X) | |